0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 6 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 9 ms)
↳12 QDP
↳13 UsableRulesReductionPairsProof (⇔, 124 ms)
↳14 QDP
↳15 MRRProof (⇔, 0 ms)
↳16 QDP
↳17 PisEmptyProof (⇔, 0 ms)
↳18 YES
flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_GA(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_GA(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_GA(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → U4_GA(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)
flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_GA(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_GA(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_GA(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → U4_GA(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)
flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)
flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → FLATTENA_IN_GA(T30)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83)) → FLATTENA_IN_GA(cons(T82, T83))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99)) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))))
No rules are removed from R.
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → FLATTENA_IN_GA(T30)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83)) → FLATTENA_IN_GA(cons(T82, T83))
POL(FLATTENA_IN_GA(x1)) = 2·x1
POL(atom(x1)) = x1
POL(cons(x1, x2)) = x1 + x2
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99)) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99)) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))))
POL(FLATTENA_IN_GA(x1)) = 2·x1
POL(cons(x1, x2)) = 2 + 2·x1 + x2